Nuprl Lemma : int_lower_ind
13,42
postcript
pdf
i
:
,
E
:({...
i
}
{u}).
E
(
i
)
(
k
:{...
i
- 1}.
E
(
k
+1)
E
(
k
))
{
k
:{...
i
}.
E
(
k
)}
latex
Up
int
2
,
int
2
Definitions
False
,
A
,
A
B
,
t
T
,
{
T
}
,
x
(
s
)
,
P
Q
,
,
{...
i
}
,
x
:
A
.
B
(
x
)
,
x
.
t
(
x
)
,
i
>
j
,
P
&
Q
,
P
Q
,
P
Q
,
WellFnd{i}(
A
;
x
,
y
.
R
(
x
;
y
))
,
P
Q
,
Dec(
P
)
Lemmas
le
wf
,
int
lower
wf
,
int
lower
well
founded
,
gt
wf
,
decidable
int
equal
origin
i:
, E:({...i}
{u}). E(i) 
(k:{...i - 1}. E(k+1) E(k)) {k:{...i}. E(k)} i:, E:({...i}{u}). E(i) (k:{...i - 1}. E(k+1) E(k)) {k:{...i}. E(k)} 
A
B
T Qx:A. B(x)
x. t(x)
Q Q
Q